\begin{tabbing}
$\forall$${\it es}$:ES, $A$, $B$, $P$, $Q$:(E$\rightarrow\mathbb{P}$), $T$, ${\it T'}$:Type, $R$:($T$$\rightarrow$${\it T'}$$\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$e$:E. ($A$($e$) $\vee$ $B$($e$)) $\Rightarrow$ (valtype($e$) $\subseteq$r $T$))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. ($P$($e$) $\vee$ $Q$($e$)) $\Rightarrow$ (valtype($e$) $\subseteq$r ${\it T'}$))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. $\neg$($A$($e$) \& $B$($e$)))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. $\neg$($P$($e$) \& $Q$($e$)))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. Dec($P$($e$)))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. Dec($A$($e$)))
\\[0ex]$\Rightarrow$ \=($\forall$$f$:(\{$e$:E$\mid$ $A$($e$)\} $\rightarrow$\{$e$:E$\mid$ $P$($e$)\} ), $g$:(\{$e$:E$\mid$ $B$($e$)\} $\rightarrow$\{$e$:E$\mid$ $Q$($e$)\} ).\+
\\[0ex]($e$.$A$($e$) $\rightarrow$$e$.$f$($e$)$\rightarrow$ $e$.$P$($e$)) with $R$
\\[0ex]$\Rightarrow$ ($e$.$B$($e$) $\rightarrow$$e$.$g$($e$)$\rightarrow$ $e$.$Q$($e$)) with $R$
\\[0ex]$\Rightarrow$ ($\exists$\=$h$:\{$e$:E$\mid$ $A$($e$) $\vee$ $B$($e$)\} $\rightarrow$\{$e$:E$\mid$ $P$($e$) $\vee$ $Q$($e$)\} \+
\\[0ex](($e$.$A$($e$) $\vee$ $B$($e$) $\rightarrow$$e$.$h$($e$)$\rightarrow$ $e$.$P$($e$) $\vee$ $Q$($e$)) with $R$
\\[0ex]\& ($\forall$$e$:\{$e$:E$\mid$ $A$($e$) $\vee$ $B$($e$)\} . $A$($e$) $\Rightarrow$ ($h$($e$) = $f$($e$)))
\\[0ex]\& ($\forall$$e$:\{$e$:E$\mid$ $A$($e$) $\vee$ $B$($e$)\} . ($\neg$$A$($e$)) $\Rightarrow$ ($h$($e$) = $g$($e$))))))
\-\-
\end{tabbing}